i:Id, T:Type, v:T, x:Id. @i: x:T initially x = v  Dsys 

latex

Definitions	Dsys, @i: x:T initially x = v, if b t else f fi, eqof(d), IdDeq, MsgA, x : t initially x = v, x:A. B(x), , t  T, Id
Lemmas	Id wf, ma-empty wf, ma-single-init wf, msga wf, id-deq wf, eqof wf, ifthenelse wf